Inference at * 1 1 
Iof proof for Lemma can-apply-mu':



1. A : Type
2. P : A
3. x:A. Dec(n:. ((P(x,n))))
4. x : A
5. Top
6. i:. ((P(x,i)))
7. n:. ((P(x,n)))
  False 

latex

 by (ExRepD) 
CollapseTHEN ((InstHyp [n] (-3)) 
CollapseTHEN (Auto)) 

latex

C.

Definitions

x:A. B(x), x:A  B(x), x:A. B(x), A, P  Q, False